T:Type, L, L1, L2:T List.
interleaving(T;L1;L2;L)  (P:(||L||). L1 = filter2(P;L) & L2 = filter2(i.P(i);L)) 

latex

Definitions

t  T, x:A. B(x), Prop, P & Q, , {i..j}, x:A. B(x), interleaving(T;L1;L2;L), P  Q, P  Q, P  Q, False, A, AB, ij, t  ...$L, ||as||, , {T}, SQType(T), b, filter2(P;L), tl(l), l[i], A & B, P  Q, true, i=j, if b t else f fi, i  j < k, b, Unit, hd(l), i<j, ij, True, T, false

Lemmas

interleaving symmetry, cons interleaving, bfalse wf, squash wf, true wf, select wf, length wf2, cons filter2, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, btrue wf, not wf, assert wf, tl wf, interleaving of cons, filter2 wf, bnot wf, le wf, nat wf, cons one one, member wf, nil interleaving, length zero, non neg length, length nil, length wf1, interleaving wf, int seg wf, bool wf